Inference at * 1 1 
Iof proof for Lemma add functionality wrt le:



1. i1 : 
2. i2 : 
3. j2 : 
4. i2  j2
  j1:. (i1  j1)  ((i1+i2)  (j1+j2)) 

latex

 by (RA (IntInd 1)) 

latex

 1: 

 1: 1. i2 : 
 1: 2. j2 : 
 1: 3. i2  j2
 1: 4. i1 : 
 1: 5. i1 < 0
 1: 6. j1:. ((i1+1)  j1)  ((i1+1+i2)  (j1+j2))
 1: 7. j1 : 
 1: 8. i1  j1
 1:   (i1+i2)  (j1+j2)
 2: 

 2: 1. i2 : 
 2: 2. j2 : 
 2: 3. i2  j2
 2: 4. j1 : 
 2: 5. 0  j1
 2:   (0+i2)  (j1+j2)
 3: 

 3: 1. i2 : 
 3: 2. j2 : 
 3: 3. i2  j2
 3: 4. i1 : 
 3: 5. 0 < i1
 3: 6. j1:. ((i1 - 1)  j1)  (((i1 - 1)+i2)  (j1+j2))
 3: 7. j1 : 
 3: 8. i1  j1
 3:   (i1+i2)  (j1+j2)
 .

Definitions	t  T, P  Q, x:A. B(x),
Lemmas	le wf